M. Maggesi, C. P. Brogi; "A Formal Proof of Modal Completeness for Provability Logic"
メモ
特に理由が無ければより新しい
M. Maggesi, C. P. Brogi; "Mechanising Gödel–Löb Provability Logic in HOL Light"
を読むべき．
https://drops.dagstuhl.de/opus/volltexte/2021/13921/pdf/LIPIcs-ITP-2021-26.pdf
HOL Light
で
様相論理GL
の完全性を示す．
具体的にはThm1を示す．
任意の様相論理式
$ \varphi
に対し，
$ \mathsf{GL} \vdash A
$ \iff
非反射的かつ推移的な任意の有限フレーム
$ \mathcal{F}
で
$ \mathcal{F} \models A
#定理証明支援系での論理の形式化